Nuprl Lemma : rv-disjoint-rv-add2 11,40
p:FinProbSpace, n:, X, Y, Z:RandomVariable(p;n).
rv-disjoint(p;n;Y;X)  rv-disjoint(p;n;Z;X)  rv-disjoint(p;n;Y + Z;X) 
latex

Definitionst  T, x:A. B(x), X + Y, P  Q, FinProbSpace, , RandomVariable(p;n), rv-disjoint(p;n;X;Y), False, A, A  B, , {x:A| B(x)} 
Lemmasrv-disjoint wf, random-variable wf, nat wf, finite-prob-space wf, rv-disjoint-rv-add, rv-disjoint-symmetry, rv-add wf

origin